(declare-fun _substvar_15_ () Bool)
(declare-fun _substvar_23_ () Bool)
(declare-const r5 Real)
(assert (not (exists ((q3 Bool) (q4 Real)) (< r5 0.0 r5 0.4467963 472603.7747))))
(assert _substvar_23_)
(assert _substvar_15_)
(check-sat)
